i:Id, k:Knd. (hasloc(k;i))  ((isrcv(k))  (destination(lnk(k)) = i)) 

latex

Definitions	t  T, True, P  Q, x:A. B(x), destination(l), Id, , False, A, P  Q, P & Q, P  Q, a = b, b, b, outl(x), IdLnk, t.1, x. t(x), Knd, lnk(k), isrcv(k), hasloc(k;i), P  Q, Dec(P)
Lemmas	decidable equal Id, Knd wf, pi1 wf, IdLnk wf, false wf, iff functionality wrt iff, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, bnot wf, assert wf, eq id wf, not wf, true wf, Id wf, ldst wf